$M$.pre($a$,$s$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$P$ != ($M$.2.2.2).1($a$) $\Rightarrow$ $\uparrow$($P$($s$))